package bcontractor.propositional.minisat;

import java.util.regex.Matcher;
import java.util.regex.Pattern;

public class MiniSatOutputParser {

    private static final Pattern SATISFIABLE_PATTERN = Pattern.compile("(?m)^SATISFIABLE$");

    private static final Pattern VARIABLES_PATTERN = Pattern.compile("Number of variables:\\s*(\\d+)");

    private static final Pattern CLAUSES_PATTERN = Pattern.compile("Number of clauses:\\s*(\\d+)");

    private static final Pattern PARSE_TIME_PATTERN = Pattern.compile("Number of variables:\\s*(\\d+(?:\\.\\d+)?)");

    private static final Pattern RESTARTS_PATTERN = Pattern.compile("restarts\\s*: (\\d+)");

    private static final Pattern CONFLICTS_PATTERN = Pattern.compile("conflicts\\s*: (\\d+)");

    private static final Pattern DECISIONS_PATTERN = Pattern.compile("decisions\\s*: (\\d+)");

    private static final Pattern PROPAGATIONS_PATTERN = Pattern.compile("propagations\\s*: (\\d+)");

    private static final Pattern CONFLICT_LITERALS_PATTERN = Pattern.compile("conflict literals\\s*: (\\d+)");

    private static final Pattern MEMORY_USED_PATTERN = Pattern.compile("Memory used\\s*: (\\d+(?:\\.\\d+)?)");

    private static final Pattern CPU_TIME_PATTERN = Pattern.compile("CPU time\\s*: (\\d+(?:\\.\\d+)?)");

    public MiniSatResult parseOutput(String output) {
        MiniSatResult result = new MiniSatResult();
        result.setSatisfiable(SATISFIABLE_PATTERN.matcher(output).find());
        result.setVariables(this.parseInteger(output, VARIABLES_PATTERN));
        result.setClauses(this.parseInteger(output, CLAUSES_PATTERN));
        result.setParseTime(this.parseDouble(output, PARSE_TIME_PATTERN));
        result.setRestarts(this.parseInteger(output, RESTARTS_PATTERN));
        result.setConflicts(this.parseInteger(output, CONFLICTS_PATTERN));
        result.setDecisions(this.parseInteger(output, DECISIONS_PATTERN));
        result.setPropagations(this.parseInteger(output, PROPAGATIONS_PATTERN));
        result.setConflictLiterals(this.parseInteger(output, CONFLICT_LITERALS_PATTERN));
        result.setMemoryUsed(this.parseDouble(output, MEMORY_USED_PATTERN));
        result.setCpuTime(this.parseDouble(output, CPU_TIME_PATTERN));
        return result;
    }

    private Double parseDouble(String output, Pattern pattern) {
        Matcher matcher = pattern.matcher(output);
        if (!matcher.find()) {
            throw new RuntimeException(String.format("Padrão %s não encontrado na saída: %s", pattern, output));
        }
        return Double.parseDouble(matcher.group(1));
    }

    private Integer parseInteger(String output, Pattern pattern) {
        Matcher matcher = pattern.matcher(output);
        if (!matcher.find()) {
            throw new RuntimeException(String.format("Padrão %s não encontrado na saída: %s", pattern, output));
        }
        return Integer.parseInt(matcher.group(1));
    }
}
